/*******************************************************************************
* SAT4J: a SATisfiability library for Java Copyright (C) 2004-2008 Daniel Le Berre
*
* All rights reserved. This program and the accompanying materials
* are made available under the terms of the Eclipse Public License v1.0
* which accompanies this distribution, and is available at
* http://www.eclipse.org/legal/epl-v10.html
*
* Alternatively, the contents of this file may be used under the terms of
* either the GNU Lesser General Public License Version 2.1 or later (the
* "LGPL"), in which case the provisions of the LGPL are applicable instead
* of those above. If you wish to allow use of your version of this file only
* under the terms of the LGPL, and not to allow others to use your version of
* this file under the terms of the EPL, indicate your decision by deleting
* the provisions above and replace them with the notice and other provisions
* required by the LGPL. If you do not delete the provisions above, a recipient
* may use your version of this file under the terms of the EPL or the LGPL.
* 
* Based on the original MiniSat specification from:
* 
* An extensible SAT solver. Niklas Een and Niklas Sorensson. Proceedings of the
* Sixth International Conference on Theory and Applications of Satisfiability
* Testing, LNCS 2919, pp 502-518, 2003.
*
* See www.minisat.se for the original solver in C++.
* 
*******************************************************************************/
package org.sat4j;

import java.io.BufferedReader;
import java.io.FileNotFoundException;
import java.io.IOException;
import java.io.InputStreamReader;
import java.io.ObjectInputStream;
import java.io.PrintWriter;
import java.io.Serializable;
import java.net.URL;
import java.util.Properties;

import org.sat4j.core.ASolverFactory;
import org.sat4j.reader.ParseFormatException;
import org.sat4j.reader.Reader;
import org.sat4j.specs.ContradictionException;
import org.sat4j.specs.IProblem;
import org.sat4j.specs.ISolver;
import org.sat4j.specs.TimeoutException;

/**
 * That class is used by launchers used to solve decision problems, i.e.
 * problems with YES/NO/UNKNOWN answers.
 * 
 * @author leberre
 * 
 */
public abstract class AbstractLauncher implements Serializable {

    /**
	 * 
	 */
	private static final long serialVersionUID = 1L;

	public static final String SOLUTION_PREFIX = "v "; //$NON-NLS-1$

    public static final String ANSWER_PREFIX = "s "; //$NON-NLS-1$

    public static final String COMMENT_PREFIX = "c "; //$NON-NLS-1$

    private long beginTime;
    
    private ExitCode exitCode = ExitCode.UNKNOWN;

    protected Reader reader;

    private transient PrintWriter out = new PrintWriter(System.out, true);
    
    protected transient Thread shutdownHook = new Thread() {
        @Override
        public void run() {
            displayResult();
        }
    };

    protected ISolver solver;

    private boolean silent = false;

    protected AbstractLauncher() {
        Runtime.getRuntime().addShutdownHook(shutdownHook);
    }

    protected void displayResult() {
        if (solver != null) {
            double wallclocktime = (System.currentTimeMillis() - beginTime) / 1000.0;
            solver.printStat(out, COMMENT_PREFIX);
            out.println(ANSWER_PREFIX + exitCode);
            if (exitCode == ExitCode.SATISFIABLE) {
                int[] model = solver.model();
                out.print(SOLUTION_PREFIX);
                reader.decode(model, out);
                out.println();
            }
            log("Total wall clock time (in seconds) : " + wallclocktime); //$NON-NLS-1$
        }
    }

    public abstract void usage();

    /**
     * @throws IOException
     */
    protected final void displayHeader() {
        displayLicense();
        URL url = AbstractLauncher.class.getResource("/sat4j.version"); //$NON-NLS-1$
        if (url == null) {
            log("no version file found!!!"); //$NON-NLS-1$			
        } else {
            BufferedReader in = null;
            try {
                in = new BufferedReader(new InputStreamReader(url
                        .openStream()));
                log("version " + in.readLine()); //$NON-NLS-1$
            } catch (IOException e) {
                 log("c ERROR: "+e.getMessage());
            } finally {
                if (in!=null) {
                    try {
                        in.close();
                    } catch (IOException e) {
                        log("c ERROR: "+e.getMessage());
                    }
                }
            }
        }
        Properties prop = System.getProperties();
        String[] infoskeys = {
                "sun.arch.data.model", "java.version", "os.name", "os.version", "os.arch" }; //$NON-NLS-1$//$NON-NLS-2$ //$NON-NLS-3$ //$NON-NLS-4$//$NON-NLS-5$
        for (String key : infoskeys) {
            log(key + "\t" + prop.getProperty(key)); //$NON-NLS-1$
        }
        Runtime runtime = Runtime.getRuntime();
        log("Free memory " + runtime.freeMemory()); //$NON-NLS-1$
        log("Max memory " + runtime.maxMemory()); //$NON-NLS-1$
        log("Total memory " + runtime.totalMemory()); //$NON-NLS-1$
        log("Number of processors " + runtime.availableProcessors()); //$NON-NLS-1$
    }

    public void displayLicense() {
        log("SAT4J: a SATisfiability library for Java (c) 2004-2008 Daniel Le Berre"); //$NON-NLS-1$
        log("This is free software under the dual EPL/GNU LGPL licenses."); //$NON-NLS-1$
        log("See www.sat4j.org for details."); //$NON-NLS-1$
    }

    /**
     * Reads a problem file from the command line.
     * 
     * @param problemname
     *            the fully qualified name of the problem.
     * @return a reference to the problem to solve
     * @throws FileNotFoundException
     *             if the file is not found
     * @throws ParseFormatException
     *             if the problem is not expressed using the right format
     * @throws IOException
     *             for other IO problems
     * @throws ContradictionException
     *             if the problem is found trivially unsat
     */
    protected IProblem readProblem(String problemname)
            throws FileNotFoundException, ParseFormatException, IOException,
            ContradictionException {
        log("solving " + problemname); //$NON-NLS-1$
        log("reading problem ... "); //$NON-NLS-1$
        reader = createReader(solver, problemname);
        IProblem problem = reader.parseInstance(problemname);
        log("... done. Wall clock time " //$NON-NLS-1$
                + (System.currentTimeMillis() - beginTime) / 1000.0 + "s."); //$NON-NLS-1$
        log("#vars     " + problem.nVars()); //$NON-NLS-1$
        log("#constraints  " + problem.nConstraints()); //$NON-NLS-1$
        problem.printInfos(out,COMMENT_PREFIX);    
        return problem;
    }

    protected abstract Reader createReader(ISolver theSolver, String problemname);

    public void run(String[] args) {

        try {
            displayHeader();
            solver = configureSolver(args);
            if (solver == null)
                return;
            String instanceName = getInstanceName(args);
            beginTime = System.currentTimeMillis();
            IProblem problem = readProblem(instanceName);
            try {
                solve(problem);
            } catch (TimeoutException e) {
                log("timeout"); //$NON-NLS-1$
            }
        } catch (FileNotFoundException e) {
            log("FATAL");
            e.printStackTrace();
        } catch (IOException e) {
            log("FATAL");
            e.printStackTrace();
        } catch (ContradictionException e) {
            exitCode = ExitCode.UNSATISFIABLE;
            log("(trivial inconsistency)"); //$NON-NLS-1$
        } catch (ParseFormatException e) {
            log("FATAL");
            e.printStackTrace();
        }
    }

    protected abstract String getInstanceName(String[] args);

    protected abstract ISolver configureSolver(String[] args);

    /**
     * Display messages as comments on STDOUT
     * 
     * @param message
     */
    public void log(String message) {
        if (!silent)
            out.println(COMMENT_PREFIX + message);
    }

    protected void solve(IProblem problem) throws TimeoutException {
        exitCode = problem.isSatisfiable() ? ExitCode.SATISFIABLE
                : ExitCode.UNSATISFIABLE;
    }

    /**
     * Change the value of the exit code in the Launcher
     * 
     * @param exitCode
     *            the new ExitCode
     */
    public final void setExitCode(ExitCode exitCode) {
        this.exitCode = exitCode;
    }

    /**
     * Get the value of the ExitCode
     * 
     * @return the current value of the Exitcode
     */
    public final ExitCode getExitCode() {
        return exitCode;
    }

    /**
     * Obtaining the current time spent since the beginning of the solving
     * process.
     * 
     * @return the time signature at the beginning of the run() method.
     */
    public final long getBeginTime() {
        return beginTime;
    }

    /**
     * 
     * @return the reader used to parse the instance
     */
    public final Reader getReader() {
        return reader;
    }

    /**
     * To change the output stream on which statistics are displayed. By
     * default, the solver displays everything on System.out.
     * 
     * @param out
     */
    public void setLogWriter(PrintWriter out) {
        this.out = out;
    }

    public PrintWriter getLogWriter() {
        return out;
    }

    protected void setSilent(boolean b) {
        silent = b;
    }
    
    private void readObject(ObjectInputStream stream) throws IOException, ClassNotFoundException {
        stream.defaultReadObject();
        out = new PrintWriter(System.out, true);
        shutdownHook = new Thread() {
            @Override
            public void run() {
                displayResult();
            }
        };
    }

    protected <T extends ISolver> void showAvailableSolvers(ASolverFactory<T> afactory) {
        if (afactory != null) {
            log("Available solvers: "); //$NON-NLS-1$
            String[] names = afactory.solverNames();
            for (int i = 0; i < names.length; i++) {
                log(names[i]);
            }
        }
    }
}
